In this section, we will prove
\[ \Con(\mathsf{ZF}) \to \Con(\mathsf{ZFC} + \mathsf{GCH}) \]

\subsection{Definable sets}
Recall that the \( \mathrm{V}_\alpha \) hierarchy has the property that \( \mathrm{V}_{\alpha + 1} = \mathcal P(\mathrm{V}_\alpha) \).
We will construct a universe \( \mathrm{L} \) in which we restrict to the `nice' subsets.
\begin{definition}
    A set \( x \) is said to be \emph{definable} over \( (M, \in) \) if there exist \( a_1, \dots, a_n \in M \) and a formula \( \varphi \) such that
    \[ x = \qty{z \in M \mid (M, \in) \vDash \varphi(z, a_1, \dots, a_n)} \]
    We write
    \[ \operatorname{Def}(M) = \qty{x \subseteq M \mid x \text{ is definable over } M} \]
\end{definition}
\begin{remark}
    \begin{enumerate}
        \item \( M \in \operatorname{Def}(M) \).
        \item \( M \subseteq \operatorname{Def}(M) \subseteq \mathcal P(M) \).
    \end{enumerate}
\end{remark}
This definition involves a quantification over infinitely many formulas, so is not yet fully formalised.
One method to do this is to code formulas as elements of \( \mathrm{V}_\omega \), called \emph{G\"odel codes}.
We can then use Tarski's satisfaction relation to define a formula \( \mathsf{Sat} \), and can then prove
\[ \mathsf{Sat}(M, E, \ulcorner \varphi \urcorner, x_1, \dots, x_n) \leftrightarrow (M, \in) \vDash \varphi(x_1, \dots, x_n) \]
where \( \ulcorner \varphi \urcorner \in V_\omega \) is the G\"odel code for \( \varphi \).
We will later use a different method to formalise it, but for now we will assume that this is well-defined.

\subsection{Defining the constructible universe}
We define the \( \mathrm{L}_\alpha \) hierarchy by transfinite recursion as follows.
\[ \mathrm{L}_0 = \varnothing;\quad \mathrm{L}_{\alpha + 1} = \operatorname{Def}(\mathrm{L}_\alpha);\quad \mathrm{L}_\lambda = \bigcup_{\alpha < \lambda} \mathrm{L}_\alpha;\quad \mathrm{L} = \bigcup_{\alpha \in \mathrm{Ord}} \mathrm{L}_\alpha \]
\begin{lemma}
    For any ordinals \( \alpha, \beta \),
    \begin{enumerate}
        \item if \( \beta \leq \alpha \) then \( \mathrm{L}_\beta \subseteq \mathrm{L}_\alpha \);
        \item if \( \beta < \alpha \) then \( \mathrm{L}_\beta \in \mathrm{L}_\alpha \);
        \item \( \mathrm{L}_\alpha \) is transitive;
        \item the ordinals of \( \mathrm{L}_\alpha \) are precisely \( \alpha \);
        \item \( \mathrm{L} \) is transitive and \( \mathrm{Ord} \subseteq \mathrm{L} \).
    \end{enumerate}
\end{lemma}
\begin{definition}
    Let \( T \) be a set of axioms in \( \mathcal L_\in \), and let \( W \) be a class.
    Then \( W \) is called an \emph{inner model} of \( T \) if
    \begin{enumerate}
        \item \( W \) is a transitive class;
        \item \( \mathrm{Ord} \subseteq W \);
        \item \( T^W \) is true; that is, for every formula \( \varphi \) in \( T \), we have \( \varphi^W \).
    \end{enumerate}
\end{definition}
\begin{theorem}
    \( \mathrm{L} \) is an inner model of \( \mathsf{ZF} \).
\end{theorem}
This is a theorem scheme; for every axiom of \( \mathsf{ZF} \), we can prove its relativisation to \( \mathrm{L} \).
\begin{proof}
    By the previous lemma, it suffices to check that \( \mathsf{ZF}^{\mathrm{L}} \) holds.
    \begin{itemize}
        \item Since \( \mathrm{L} \) is transitive, \( \mathrm{L} \) satisfies extensionality and foundation.
        \item For the axiom of empty set, we use the fact that \( \varnothing^{\mathrm{L}} = \varnothing = \mathrm{L}_0 \in \mathrm{L} \).
        \item For pairing, given \( a, b \in \mathrm{L} \), we must show \( \qty{a, b} \in \mathrm{L} \).
        Fix \( \alpha \) such that \( a, b \in \mathrm{L}_\alpha \).
        Then
        \[ \qty{a, b} = \qty{x \in \mathrm{L}_\alpha \mid (\mathrm{L}_\alpha, \in) \vDash x = a \vee x = b} \in \operatorname{Def}(\mathrm{L}_\alpha) \]
        \item For union, let \( a \in \mathrm{L}_\alpha \).
        By transitivity, \( \bigcup a \subseteq \mathrm{L}_\alpha \).
        Then
        \[ \bigcup a = \qty{x \in \mathrm{L}_\alpha \mid (\mathrm{L}_\alpha, \in) \vDash \exists z.\, (z \in a \wedge x \in z)} \in \operatorname{Def}(\mathrm{L}_\alpha) \]
        \item For infinity, note that
        \[ \omega = \qty{n \in \mathrm{L}_\omega \mid (\mathrm{L}_\omega, \in) \vDash n \in \mathrm{Ord}} \in \operatorname{Def}(\mathrm{L}_\alpha) \]
        \item Consider separation.
        Let \( \varphi \) be a formula, and let \( a, \vb u \in \mathrm{L}_\alpha \).
        We claim that
        \[ b = \qty{x \in a \mid \varphi^{\mathrm{L}}(x, \vb u)} \in \mathrm{L} \]
        This implicitly uses the fact that \( \mathrm{L} \) is definable.
        Using the reflection theorem, there is \( \beta > \alpha \) such that
        \[ \mathsf{ZF} \vdash \forall x \in \mathrm{L}_\beta.\, (\varphi^{\mathrm{L}}(x, \vb u) \leftrightarrow \varphi^{\mathrm{L}_\beta}(x, \vb u)) \]
        Moreover, \( \varphi^{\mathrm{L}_\beta}(x, \vb u) \) holds if and only if \( (\mathrm{L}_\beta, \in) \vDash \varphi(x, \vb u) \).
        We thus obtain
        \[ \qty{x \in a \mid \varphi^{\mathrm{L}}(x, \vb u)} = \qty{x \in a \mid \varphi^{\mathrm{L}_\beta}(x, \vb u)} = \qty{x \in \mathrm{L}_\beta \mid (\mathrm{L}_\beta, \in) \vDash \varphi(x, \vb u) \wedge x \in a} \in \operatorname{Def}(\mathrm{L}_\beta) \]
        \item We now consider replacement.
        It suffices to show that if \( a \in \mathrm{L} \) and \( f : a \to \mathrm{L} \) is a definable function, then there exists \( \gamma \in \mathrm{Ord} \) such that \( f '' a \subseteq \mathrm{L}_\gamma \), since then we can use separation.
        First, observe that for every \( x \in a \), there exists \( \beta \in \mathrm{Ord} \) such that \( f(x) \in \mathrm{L}_\beta \).
        Using replacement in \( \mathrm{V} \), there exists an ordinal \( \gamma \) such that for all \( x \in a \), there exists \( \beta < \gamma \) such that \( f(x) \in \mathrm{L}_\beta \).
        As \( \mathrm{L}_\beta \subseteq \mathrm{L}_\gamma \), we thus obtain for all \( x \in a \) that \( f(x) \in \mathrm{L}_\gamma \).
        \item Finally, consider the axiom of power set.
        It suffices to prove that if \( x \in \mathrm{L} \) then \( \mathcal P(x) \cap \mathrm{L} \in \mathrm{L} \).
        Take \( x \in \mathrm{L} \).
        Using replacement in \( \mathrm{V} \), we can fix an ordinal \( \gamma \) such that \( \mathcal P(x) \cap \mathrm{L} \subseteq \mathrm{L}_\gamma \).
        Then
        \[ \mathcal P(x) \cap \mathrm{L} = \qty{z \in \mathrm{L}_\gamma \mid (\mathrm{L}, \in) \vDash z \subseteq x} \in \operatorname{Def}(\mathrm{L}_\gamma) \]
    \end{itemize}
\end{proof}

\subsection{G\"odel functions}
We will now formally define \( \mathrm{L} \).
For clarity, we will define the ordered triple \( \langle a, b, c \rangle \) to be \( \langle a, \langle b, c \rangle \rangle \).
\begin{definition}
    The \emph{G\"odel functions} are the following collection of functions on two variables.
    \begin{enumerate}
        \item \( \mathcal F_1(x, y) = \qty{x, y} \);
        \item \( \mathcal F_2(x, y) = \bigcup x \);
        \item \( \mathcal F_3(x, y) = x \setminus y \);
        \item \( \mathcal F_4(x, y) = x \times y \);
        \item \( \mathcal F_5(x, y) = \dom x = \qty{\pi_1(z) \mid z \in x \wedge z \text{ is an ordered pair}} \);
        \item \( \mathcal F_6(x, y) = \ran x = \qty{\pi_2(z) \mid z \in x \wedge z \text{ is an ordered pair}} \);
        \item \( \mathcal F_7(x, y) = \qty{\langle u, v, w \rangle \mid \langle u, v \rangle \in x, w \in y} \);
        \item \( \mathcal F_8(x, y) = \qty{\langle u, w, v \rangle \mid \langle u, v \rangle \in x, w \in y} \);
        \item \( \mathcal F_9(x, y) = \qty{\langle v, u \rangle \in y \times x \mid u = v} \);
        \item \( \mathcal F_{10}(x, y) = \qty{\langle v, u \rangle \in y \times x \mid u \in v} \).
    \end{enumerate}
\end{definition}
\begin{proposition}
    The following can all be written as a finite combination of G\"odel functions (i)--(vii).
    \[ \qty{x};\quad x \cup y;\quad x \cap y;\quad \langle x, y \rangle;\quad \langle x, y, z \rangle \]
\end{proposition}
\begin{proposition}
    For every \( i \in \qty{1, \dots, 10} \), the statement \( z = \mathcal F_i(x, y) \) can be written using a \( \Delta_0 \) formula.
    Hence, these formulas are absolute.
\end{proposition}
\begin{lemma}[G\"odel normal form]
    For every \( \Delta_0 \) formula \( \varphi(x_1, \dots, x_n) \) with free variables contained in \( \qty{x_1, \dots, x_n} \), there is a term \( \mathcal F_\varphi \) built from the symbols \( \mathcal F_1, \dots, \mathcal F_{10} \) such that
    \[ \mathsf{ZF} \vdash \forall a_1, \dots, a_n.\, \mathcal F_\varphi(a_1, \dots, a_n) = \qty{\langle x_n, \dots, x_1 \rangle \in a_n \times \dots \times a_1 \mid \varphi(x_1, \dots, x_n)} \]
\end{lemma}
\begin{remark}
    \begin{enumerate}
        \item The reversed order of the free variables is done purely for technical reasons.
        \item \( \mathcal F_2 \) will correspond to disjunction for \( \Delta_0 \) formulas, intersection will correspond to intersection, \( \mathcal F_3 \) will give negation, and \( \mathcal F_9 \) and \( \mathcal F_{10} \) will give atomic formulas.
        \item \( \mathcal F_7 \) and \( \mathcal F_8 \) will deal with ordered \( n \)-tuples.
        The triple \( \langle x_1, x_2, x_3 \rangle \), this is formed using \( x_1 \) and \( \langle x_2, x_3 \rangle \).
        However, it cannot be formed using \( \langle x_1, x_2 \rangle \) and \( x_3 \).
    \end{enumerate}
\end{remark}
\begin{proof}
    We show this by induction on the class \( \Delta_0 \).
    We call a formula \( \varphi \) a \emph{termed formula} if the conclusion of the lemma holds for \( \varphi \); we aim to show that every \( \Delta_0 \)-formula is a termed formula.
    We will only use the logical symbols \( \wedge, \vee, \neg, \exists \), and the only occurrence of existential quantification will be in formulas of the form
    \[ \varphi(x_1, \dots, x_n) \equiv \exists x_{n+1} \in x_j.\, \psi(x_1, \dots, x_{n+1}) \]
    where \( j \leq m \leq n \).
    For example, we allow \( \exists x_3 \in x_1.\, (x_1 \in x_2 \wedge x_3 = x_1) \), but we disallow \( \exists x_1 \in x_2.\, \psi \) and \( \exists x_3 \in x_1.\, (x_3 \in x_2 \wedge \exists x_4 \in x_1.\, \psi) \).
    Every \( \Delta_0 \)-formula is equivalent to one of this form.
    We allow for dummy variables, so \( \varphi(x_1, x_2) \equiv x_1 \in x_2 \) and \( \varphi(x_1, x_2, x_3) \equiv x_1 \in x_2 \) are distinct.
    This proof will take place in four parts: first some logical points, then we consider propositional formulas, then atomic formulas, and finally bounded existentials.

    \emph{Part (i): logical points.}
    We make the following remarks.
    \begin{itemize}
        \item If \( \mathsf{ZF} \vdash \varphi(\vb x) \leftrightarrow \psi(\vb x) \) and \( \varphi(\vb x) \) is a termed formula, then \( \psi \) is also a termed formula.
        This is immediate from the definition, since we can let \( \mathcal F_\psi = \mathcal F_\varphi \).
        \item For all \( m, n \), if \( \varphi(x_1, \dots, x_n) \equiv \psi(x_1, \dots, x_m) \) and \( \psi \) is a termed formula, then so is \( \varphi \).
        If \( n \geq m \), we can show this by induction on \( n \).
        The base case \( n = m \) is trivial.
        For the inductive step, suppose
        \[ \varphi(x_1, \dots, x_{n+1}) \equiv \psi(x_1, \dots, x_m) \]
        Then, we can write
        \[ \varphi(x_1, \dots, x_{n+1}) \equiv \theta(x_1, \dots, x_n) \]
        where \( \theta \) is a termed formula.
        Then
        \[ \mathcal F_\varphi(a_1, \dots, a_n, a_{n+1}) = a_{n+1} \times \mathcal F_\theta(a_1, \dots, a_n) = \mathcal F_4(a_{n+1}, \mathcal F_\theta(a_1, \dots, a_n)) \]
        giving the result by the inductive hypothesis.
        This is the reason for reversing the order: because the ordered triple \( \langle x, y, z \rangle \) is \( \langle x, \langle y, z \rangle \rangle \), the map
        \[ \qty{\langle x_1, x_2 \rangle \in a_1 \times a_2 \mid \theta(x_1, x_2)} \mapsto \qty{\langle x_1, x_2, x_3 \rangle \in a_1 \times a_2 \times a_3 \mid \theta(x_1, x_2)} \]
        is much more complicated to implement in G\"odel functions.
        We prove the case \( n \leq m \) by induction; if
        \[ \varphi(x_1, \dots, x_{n-1}) \equiv \psi(x_1, \dots, x_m) \]
        then
        \[ \varphi(x_1, \dots, x_{n-1}) \equiv \theta(x_1, \dots, x_n) \]
        and
        \[ \qty{0} = \qty{\mathcal F_3(a_1, a_1)} = \mathcal F_1(\mathcal F_3(a_1, a_1), \mathcal F_3(a_1, a_1)) \]
        Then
        \begin{align*}
            \mathcal F_\varphi(a_1, \dots, a_{n-1}) &= \qty{\langle x_{n-1}, \dots, x_1 \rangle \in a_{n-1} \times \dots \times a_1 \mid \varphi(x_1, \dots, x_{n-1})} \\
            &= \ran(\qty{\langle 0, x_{n-1}, \dots, x_1 \rangle \in \qty{0} \times a_{n-1} \times \dots \times a_1 \mid \theta(x_1, \dots, x_{n-1}, 0)}) \\
            &= \mathcal F_6(\mathcal F_\theta(a_1, \dots, a_{n-1}), \mathcal F_1(\mathcal F_3(a_1, a_1), \mathcal F_3(a_1, a_1)), a_1)
        \end{align*}
        \item If \( \psi(x_1, \dots, x_n) \) is a termed formula and
        \[ \varphi(x_1, \dots, x_{n+1}) = \psi(x_1, \dots, x_{n-1}, x_{n+1}/x_n) \]
        then \( \varphi \) is a termed formula.
        First, if \( n = 1 \), we have a termed formula \( \psi(x_1) \) and consider \( \psi(x_2/x_1) \).
        Then
        \begin{align*}
            \mathcal F_\varphi(a_1, a_2) &= \qty{\langle x_2, x_1 \rangle \in a_2 \times a_1 \mid \psi(x_2)} \\
            &= \qty{\langle x_2, x_1 \rangle \mid x_1 \in a_1 \wedge x_2 \in \mathcal F_\psi(a_2)} \\
            &= \mathcal F_\psi(a_2) \times a_1 \\
            &= \mathcal F_4(\mathcal F_\psi(a_2), a_1)
        \end{align*}
        If \( n > 1 \), we have
        \begin{align*}
            \mathcal F_\varphi(a_1, \dots, a_{n+1}) &= \qty{\langle x_{n+1}, \dots, x_1 \rangle \mid x_n \in a_n \wedge \langle x_{n+1}, x_{n-1}, \dots, x_1 \rangle \in \mathcal F_\psi(a_1, \dots, a_{n-1}, a_{n+1})} \\
            &= \mathcal F_8(\mathcal F_\psi(a_1, \dots, a_{n-1}, a_{n+1}), a_n)
        \end{align*}
        \item If \( \psi(x_1, x_2) \) is a termed formula, and
        \[ \varphi(x_1, \dots, x_n) \equiv \psi(x_{n-1}/x_1, x_n/x_2) \]
        then \( \varphi \) is a termed formula.
        This is trivial if \( n = 2 \), so we assume \( n > 2 \).
        Then
        \begin{align*}
            \mathcal F_\varphi(a_1, \dots, a_n) &= \qty{\langle x_n, \dots, x_1 \rangle \in a_n \times \dots \times a_1 \mid \langle x_n, x_{n-1} \rangle \in \mathcal F_\psi(a_{n-1}, a_n)} \\
            &= \mathcal F_7(\mathcal F_\psi(a_{n-1}, a_n), a_{n-2} \times \dots \times a_1)
        \end{align*}
    \end{itemize}

    \emph{Part (ii): propositional connectives.}
    \begin{itemize}
        \item If \( \varphi \) is a termed formula, then so is \( \neg\varphi \).
        \[ \mathcal F_{\neg\varphi}(a_1, \dots, a_n) = (a_n \times \dots \times a_1) \setminus \mathcal F_\varphi(a_1, \dots, a_n) \]
        \item If \( \varphi, \psi \) are termed formulas, then so is \( \varphi \vee \psi \).
        \[ \mathcal F_{\varphi \vee \psi}(a_1, \dots, a_n) = \mathcal F_\varphi(a_1, \dots, a_n) \cup \mathcal F_\psi(a_1, \dots, a_n) \]
        It is easy to see that unions can be formed using G\"odel functions.
        \item Conjunctions are similar to disjunctions.
        \[ \mathcal F_{\varphi \wedge \psi}(a_1, \dots, a_n) = \mathcal F_\varphi(a_1, \dots, a_n) \cap \mathcal F_\psi(a_1, \dots, a_n) \]
    \end{itemize}

    \emph{Part (iii): atomic formulas.}
    \begin{itemize}
        \item Consider \( \varphi(x_1, \dots, x_n) \equiv x_i = x_j \).
        We show that this is a termed formula for all \( i, j \leq n \).
        Suppose \( i = 1 \) and \( j = 2 \).
        In this case,
        \[ \mathcal F_9(a_1, a_2) = \qty{\langle x_2, x_1 \rangle \in a_2 \times a_1 \mid x_1 = x_2} \]
        so \( \mathcal F_\varphi \) is formed using \( \mathcal F_9 \) and the discussion on dummy variables.
        Now suppose \( j \geq i \).
        We prove this by induction.
        First, if \( i = j \), then
        \[ \mathcal F_\varphi = \qty{\langle x_n, \dots, x_1 \rangle \in a_n \times \dots \times a_1 \mid x_i = x_i} = a_n \times \dots \times a_1 \]
        Now, if \( j = i + 1 \), we let
        \[ \theta(x_1, \dots, x_{i+1}) = (x_1 = x_2)[x_i/x_1, x_{i+1}/x_2] \]
        This is a termed formula by the result on substitutions.
        We thus obtain \( \mathcal F_\varphi \) by adding the required dummy variables.
        Now suppose we have \( \varphi(x_1, \dots, x_n) \equiv x_i = x_{j+1} \).
        Then we can write
        \[ \varphi(x_1, \dots, x_{j+1}) = (x_i, x_j)[x_{j+1}, x_j] \]
        which is a termed formula by substitution.
        This concludes the case \( i \leq j \) by induction.
        Finally, suppose \( i > j \).
        As \( x_i = x_j \) is logically equivalent to \( x_j = x_i \), which is a termed formula, \( \varphi \) is also a termed formula.
        \item Now consider \( \varphi(x_1, \dots, x_n) \equiv x_i \in x_j \).
        As with equality, we first consider the case \( i = 1, j = 2 \).
        In this case, we can form \( \mathcal F_{10} \) with dummy variables.
        If \( i = j \), the formula is always false, so we have
        \[ \mathcal F_\varphi(a_1, \dots, a_n) = \varnothing = a_1 \setminus a_1 = \mathcal F_3(a_1, a_1) \]
        Now, let
        \[ \psi(x_1, \dots, x_{n+2}) \equiv (x_i = x_{n+1}) \wedge (x_j = x_{n+2}) \wedge (x_{n+1} \in x_{n+2}) \]
        We note that \( x_{n+1} \in x_{n+2} \) is a termed formula as it is given by the substitution \( (x_1 \in x_2)[x_{n+1}/x_1, x_{n+2}/x_2] \).
        The equalities are termed formulas as above, so \( \psi \) is a termed formula.
        Then
        \begin{align*}
            \mathcal F_\varphi(a_1, \dots, a_n) &= \ran\ran\{\langle x_{n+2}, \dots, x_1\rangle \times a_j \times a_i \times a_n \times \dots \times a_1 \\&\quad\quad\quad\mid x_i = x_{n+1} \wedge x_j = x_{n+2} \wedge x_{n+1} \in x_{n+2}\} \\
            &= \mathcal F_6(\mathcal F_6(\mathcal F_\psi(a_1, \dots, a_n), a_1), a_1)
        \end{align*}
    \end{itemize}

    \emph{Part (iv): bounded quantifiers.}
    We required that the only occurrence of \( \exists \) was in the form
    \[ \varphi(x_1, \dots, x_n) \equiv \exists x_{m+1} \in x_j.\, \psi(x_1, \dots, x_{m+1}) \]
    where \( j \leq m \leq n \).
    Due to this restriction, it suffices to show that if \( \psi(x_1, \dots, x_{n+1}) \) is a termed formula, then so is the formula
    \[ \varphi(x_1, \dots, x_n) \equiv \exists x_{n+1} \in x_j.\, \psi(x_1, \dots, x_{n+1}) \]
    Let \( \theta(x_1, \dots, x_{n+1}) \equiv x_{n+1} \in x_j \).
    Then \( \theta \wedge \psi \) is a termed formula.
    Now
    \begin{align*}
        \mathcal F_{\theta \wedge \psi}(a_1, \dots, a_n, \mathcal F_2(a_j, a_j)) &= \mathcal F_{\theta \wedge \psi}\qty(a_1, \dots, a_n, \bigcup a_j) \\
        &= \qty{\langle x_{n+1}, \dots, x_1 \rangle \in \qty(\bigcup a_j) \times a_n \times \dots \times a_1 \mid x_{n+1} \in x_j \wedge \forall k \leq n.\, x_k \in a_k \wedge \psi(x_1, \dots, x_{n+1})}
    \end{align*}
    So
    \begin{align*}
        \ran(\mathcal F_{\theta \wedge \psi}\qty(a_1, \dots, a_n, \bigcup a_j)) &= \qty{\langle x_n, \dots, x_1 \rangle \in a_n \times \dots \times a_1 \mid \exists u.\, \langle u, x_n, \dots, x_1 \rangle \in \mathcal F_{\theta \wedge \psi}\qty(a_1, \dots, a_n, \bigcup a_j)} \\
        &= \qty{\langle x_n, \dots, x_1 \rangle \in a_n \times \dots \times a_1 \mid \exists x_{n+1} \in x_j.\, \psi(x_1, \dots, x_{n+1})}
    \end{align*}
\end{proof}
\begin{definition}
    A class \( C \) is \emph{closed under G\"odel functions} if whenever \( x, y \in C \), we have \( \mathcal F_i(x, y) \in C \) for \( i \in \qty{1, \dots, 10} \).
    Given a set \( b \), we let \( \mathrm{cl}(b) \) be the smallest set \( C \) containing \( b \) as a subset that is closed under G\"odel functions.
\end{definition}
For example, \( \mathrm{cl}(\varnothing) = \varnothing \), \( \qty{a, b} \in \mathrm{cl}(\qty{a, b}) \), and \( \mathrm{cl}(b) = \mathrm{cl}(\mathrm{cl}(b)) \).
\begin{definition}
    Let \( b \) be a set.
    Define \( \mathcal D^n(b) \) inductively by
    \[ \mathcal D^0(b) = b;\quad \mathcal D^{n+1}(b) = \qty{\mathcal F_i(x, y) \mid x, y \in \mathcal D^n(b), i \in \qty{1, \dots, 10}} \]
\end{definition}
One can easily check that \( \mathrm{cl}(b) = \bigcup_{n \in \omega} \mathcal D^n(b) \).
\begin{lemma}
    If \( M \) is a transitive class that is closed under G\"odel functions, then \( M \) satisfies \( \Delta_0 \)-separation.
\end{lemma}
\begin{proof}
    Let \( \varphi(x_1, \dots, x_n) \) be a \( \Delta_0 \)-formula, and let \( a, b_1, \dots, b_{i-1}, b_{i+1}, \dots, b_n \in M \).
    Let
    \[ Y = \qty{x_i \in a \mid \varphi(b_1, \dots, b_{i-1}, x_i, b_{i+1}, \dots, b_n)} \]
    We must show \( Y \in M \).
    Let \( \mathcal F_\varphi \) be the formula built from G\"odel's normal form theorem.
    Then for any \( c_1, \dots, c_n \in M \), we have
    \[ \mathcal F_\varphi(c_1, \dots, c_n) = \qty{\langle x_n, \dots, x_1 \rangle \in c_n \times \dots \times c_1 \mid \varphi(x_1, \dots, x_n)} \in M \]
    Hence, as \( \qty{b_j} = \mathcal F_1(b_j, b_j) \in M \), we obtain
    \[ \mathcal F_\varphi(\qty{b_1}, \dots, \qty{b_{i-1}}, a, \qty{b_{i+1}}, \dots, \qty{b_n}) \in M \]
    Then, we can show that \( Y \in M \) by taking the range \( \mathcal F_6 \) a total of \( n - i \) times and then taking the domain \( \mathcal F_5 \).
\end{proof}
\begin{theorem}
    For every transitive set \( M \), the collection of definable subsets is
    \[ \operatorname{Def}(M) = \mathrm{cl}(M \cup \qty{M}) \cap \mathcal P(M) \]
\end{theorem}
\begin{proof}
    We first prove the forward direction.
    Let \( \varphi \) be a formula.
    Then \( \varphi^M \) is \( \Delta_0 \), so there is a term \( \mathcal G \) built from the G\"odel functions \( \mathcal F_1, \dots, \mathcal F_{10} \) such that for \( a_1, \dots, a_n \in M \), we have
    \[ \qty{x \in M \mid (M, \in) \vDash \varphi(x, a_1, \dots, a_n)} = \qty{x \in M \mid \varphi^M(x, a_1, \dots, a_n)} = \mathcal G(M, a_1, \dots, a_n) \in \mathrm{cl}(M \cup \qty{M}) \]
    We now show the converse.
    We first claim that if \( \mathcal G \) is built from the G\"odel functions, then for any \( x, a_1, \dots, a_n \), the formulas
    \[ x = \mathcal G(a_1, \dots, a_n);\quad x \in \mathcal G(a_1, \dots, a_n) \]
    are \( \Delta_0 \).
    This can be proven inductively using the iterative construction of \( \mathrm{cl}(M \cup \qty{M}) \).
    For example, if \( X, Y \in \mathcal D^k(a_1, \dots, a_n) \), then \( x = \mathcal F_1(X, Y) \) is equivalent to the statement
    \[ (\forall z \in x.\, z = X \vee z = Y) \wedge (\exists w \in x.\, w = X) \wedge (\exists w \in x.\, w = Y) \]
    so the result holds for \( \mathcal F_1 \); very similar proofs show the result for both equality and membership for all other G\"odel functions.

    Let \( Z \in \mathrm{cl}(M \cup \qty{M}) \cap \mathcal P(M) \).
    Since \( Z \in \mathrm{cl}(M \cup \qty{M}) \), we can fix a term \( \mathcal G \) built from the \( \mathcal F_1, \dots, \mathcal F_{10} \) such that \( Z = \mathcal G(M, a_1, \dots, a_n) \).
    Let \( \varphi \) be a \( \Delta_0 \) formula such that \( x \in \mathcal G(M, a_1, \dots, a_n) \) if and only if \( \varphi(x, M, a_1, \dots, a_n) \).
    Then \( \mathcal G(M, a_1, \dots, a_n) = \qty{x \in M \mid \varphi(x, M, a_1, \dots, a_n)} \) as \( Z \subseteq M \).
    It therefore remains to prove that there is a formula \( \psi \) such that
    \[ \psi^M(x, a_1, \dots, a_n) \leftrightarrow \varphi(x, M, a_1, \dots, a_n) \]
    For example, we can define \( \psi \) from \( \varphi \) by the following replacements.
    \begin{enumerate}
        \item \( \exists v_i \in M \mapsto \exists v_i \);
        \item \( v_i \in M \mapsto v_i = v_i \);
        \item \( M = M \mapsto v_0 = v_0 \);
        \item \( M \in M, M \in v_i, M = v_i \mapsto v_0 \neq v_0 \).
    \end{enumerate}
    Finally, we obtain
    \[ Z = \mathcal G(M, a_1, \dots, a_n) = \qty{x \in M \mid \psi^M(x, a_1, \dots, a_n)} \in \operatorname{Def}(M) \]
\end{proof}

\subsection{The axiom of constructibility}
\begin{definition}
    The \emph{axiom of constructibility} is the statement \( \mathrm{V} = \mathrm{L} \).
    Equivalently, \( \forall x.\, \exists \alpha \in \mathrm{Ord}.\, (x \in \mathrm{L}_\alpha) \).
\end{definition}
We will show that if \( \mathsf{ZF} \) is consistent, then so is \( \mathsf{ZF} + (\mathrm{V} = \mathrm{L}) \), because \( \mathrm{L} \) is a model of \( \mathsf{ZF} + (\mathrm{V} = \mathrm{L}) \).
To do this, we will show that being constructible is absolute.
\begin{lemma}
    \( Z = \mathrm{cl}(M) \) is \( \Delta_1^{\mathsf{ZF}} \).
\end{lemma}
\begin{proof}
    The \( \Pi_1 \) definition is simply being the smallest set closed under G\"odel functions.
    More explicitly,
    \[ \forall W.\, \qty(M \cup \qty{M} \subseteq W \wedge \forall x, y \in W.\, \bigwedge_{i \leq 10} \mathcal F_i(x, y) \in W) \to Z \subseteq W \]
    The \( \Sigma_1 \) definition will use the inductive definition of the closure.
    \begin{align*}
        \exists W.\, W \text{ is a function} &\wedge \dom W = \omega \wedge Z = \bigcup \ran W \\
        &\wedge W(0) = M \wedge W(n) \subseteq W(n+1) \\
        &\wedge \qty(\forall x, y \in W(n).\, \bigwedge_{i \leq 10} \mathcal F_i(x, y) \in W(n+1)) \\
        &\wedge \qty(\forall z \in W(n+1).\, \exists x, y \in W(n).\, \bigvee_{i \leq 10} z = \mathcal F_i(x, y))
    \end{align*}
\end{proof}
\begin{lemma}
    The function mapping \( \alpha \mapsto \mathrm{L}_\alpha \) is absolute between transitive models of \( \mathsf{ZF} \).
\end{lemma}
\begin{proof}
    Define \( G : \mathrm{Ord} \times \mathrm{V} \to \mathrm{V} \) by
    \[ G(\alpha, x) = \begin{cases}
        \mathrm{cl}(x(\beta) \cup \qty{x(\beta)}) & \text{if } \alpha = \beta + 1 \text{ and } x \text{ is a function with domain } \beta \\
        \bigcup_{\beta < \alpha} x(\beta) & \text{if } \alpha \text{ is a limit} \\
        \varnothing & \text{otherwise}
    \end{cases} \]
    All of these conditions and constructions are absolute, so \( G \) is an absolute function.
    Therefore, by transfinite recursion, there exists \( F : \mathrm{Ord} \to \mathrm{V} \) where \( F : \alpha \mapsto G\qty(x, \eval{F}_\alpha) \).
    By absoluteness of transfinite recursion, \( F \) is absolute.
    Finally, \( F(\alpha) = \mathrm{L}_\alpha \) for all ordinal \( \alpha \).
\end{proof}
\begin{theorem}
    \begin{enumerate}
        \item \( \mathrm{L} \) satisfies the axiom of constructibility.
        \item \( \mathrm{L} \) is the smallest inner model of \( \mathsf{ZF} \).
        That is, if \( M \) is an inner model of \( \mathsf{ZF} \), then \( \mathrm{L} \subseteq M \).
    \end{enumerate}
\end{theorem}
\begin{proof}
    \emph{Part (i).}
    We must show
    \[ (\forall x.\, \exists \alpha \in \mathrm{Ord}.\, x \in \mathrm{L}_\alpha)^{\mathrm{L}} \]
    which is
    \[ \forall x \in \mathrm{L}.\, \exists \alpha \in \mathrm{Ord}.\, x \in (\mathrm{L}_\alpha)^{\mathrm{L}} \]
    Since the \( \mathrm{L}_\alpha \) hierarchy is absolute, \( x \in (\mathrm{L}_\alpha)^{\mathrm{L}} \) if and only if \( x \in \mathrm{L}_\alpha \).
    As \( \mathrm{L} \) contains every ordinal, if \( x \in \mathrm{L} \) then \( x \in \mathrm{L}_\alpha \) for some \( \alpha \), and thus \( x \in (\mathrm{L}_\alpha)^{\mathrm{L}} \).
    Hence \( \mathrm{L} \vDash \alpha \in \mathrm{L} \wedge x \in \mathrm{L}_\alpha \).

    \emph{Part (ii).}
    Let \( M \) be an arbitrary inner model of \( \mathsf{ZF} \).
    We construct \( \mathrm{L} \) inside \( M \) to give \( \mathrm{L}^M \).
    By absoluteness, for every \( \alpha \in M \cap \mathrm{Ord} \), we have \( \mathrm{L}_\alpha = (\mathrm{L}_\alpha)^M \).
    Thus \( \mathrm{L}_\alpha \subseteq M \) for every \( \alpha \in M \cap \mathrm{Ord} = \mathrm{Ord} \).
    Hence \( \mathrm{L} \subseteq M \) as required.
\end{proof}

\subsection{Well-ordering the universe}
We will show that \( \mathrm{L} \) satisfies a strong version of the axiom of choice, namely that there is a definable global well-order.
We will define well-orderings \( <_\alpha \) on \( \mathrm{L}_\alpha \) such that \( <_{\alpha + 1} \) \emph{end-extends} \( <_\alpha \): if \( y \in \mathrm{L}_\alpha \) and \( x \in \mathrm{L}_{\alpha + 1} \setminus \mathrm{L}_\alpha \), then \( y <_{\alpha + 1} x \).
Then we set \( <_{\mathrm{L}} = \bigcup_\alpha <_\alpha \).
\begin{theorem}
    There is a well-ordering of \( \mathrm{L} \).
\end{theorem}
\begin{proof}
    For each ordinal \( \alpha \), we will construct a well-order \( <_\alpha \) on \( \mathrm{L}_\alpha \) such that if \( \alpha < \beta \), the following hold:
    \begin{enumerate}
        \item if \( x <_\alpha y \) then \( x <_\beta y \); and
        \item if \( x \in \mathrm{L}_\alpha \) and \( y \in \mathrm{L}_\beta \setminus \mathrm{L}_\alpha \), then \( x <_\beta y \).
    \end{enumerate}
    For limit cases, we take unions:
    \[ <_\gamma = \bigcup_{\alpha < \gamma} <_\gamma \]
    We now describe the construction of \( <_{\alpha + 1} \).
    To do this, we consider the ordering on \( \mathrm{L}_\alpha \), and append the singleton \( \qty{\mathrm{L}_\alpha} \).
    We then follow that by the elements of \( \mathcal D(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \setminus (\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \).
    We then add \( \mathcal D^2(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \setminus \mathcal D(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \), and so forth.
    In order to do this, we define \( <_{\alpha + 1}^n \) for \( n \in \omega \) as follows.
    \begin{enumerate}
        \item \( <_{\alpha + 1}^0 \) is the well-ordering of \( \mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha} \) given by making \( \qty{\mathrm{L}_\alpha} \) the maximal element.
        \item Suppose that \( <_{\alpha + 1}^n \) is defined.
        We end-extend \( <_{\alpha + 1}^n \) to form \( <_{\alpha + 1}^{n + 1} \) as follows.
        Suppose \( x, y \notin \mathcal D^n(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \).
        We say \( x <_{\alpha + 1}^{n+1} \) if either
        \begin{enumerate}
            \item the least \( i \leq 10 \) such that \( \exists u, v \in \mathcal D^n(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \) with \( x = \mathcal F_i(u, v) \) is less than the least \( i \leq 10 \) such that \( \exists u, v \in \mathcal D^n(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \) with \( y = \mathcal F_i(u, v) \); or
            \item these indices \( i \) are equal, and the \( <_{\alpha + 1}^n \)-least \( u \in \mathcal D^n(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \) such that there exists \( v \in \mathcal D^n(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \) with \( x = \mathcal F_i(u, v) \) is less than the \( <_{\alpha + 1}^n \)-least \( u \in \mathcal D^n(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \) such that there exists \( v \in \mathcal D^n(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \) with \( y = \mathcal F_i(u, v) \); or
            \item both of these coincide, and \( <_{\alpha + 1}^n \)-least \( v \in \mathcal D^n(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \) with \( x = \mathcal F_i(u, v) \) is less than the least \( v \in \mathcal D^n(\mathrm{L}_\alpha \cup \qty{\mathrm{L}_\alpha}) \) with \( y = \mathcal F_i(u, v) \).
        \end{enumerate}
    \end{enumerate}
\end{proof}
The restriction of \( <_{\mathrm{L}} \) to any set \( x \in \mathrm{L} \) is a well-ordering of \( x \).
Since every set can be well-ordered, the axiom of choice holds.
\begin{lemma}
    The relation \( <_{\mathrm{L}} \) is \( \Sigma_1 \)-definable.
    Moreover, for every limit ordinal \( \delta \) and \( y \in \mathrm{L}_\delta \), we have \( x <_{\mathrm{L}} y \) if and only if \( x \in \mathrm{L}_\delta \) and \( (\mathrm{L}_\delta, \in) \vDash x <_{\mathrm{L}} y \).
\end{lemma}

\subsection{The generalised continuum hypothesis in \texorpdfstring{\( \mathrm{L} \)}{L}}
\begin{lemma}
    (\( \mathsf{ZFC} \))
    \begin{enumerate}
        \item For all \( n \in \omega \), we have \( \mathrm{L}_n = \mathrm{V}_n \).
        \item If \( M \) is infinite, then \( \abs{M} = \abs{\operatorname{Def}(M)} \).
        \item If \( \alpha \) is an ordinal, then \( \abs{\mathrm{L}_\alpha} = \abs{\alpha} \).
    \end{enumerate}
\end{lemma}
\begin{lemma}[G\"odel's condensation lemma]
    For every limit ordinal \( \delta \), if \( (M, \in) \prec (L_\delta, \in) \), then there exists some \( \beta \leq \delta \) such that \( (M, \in) \cong (\mathrm{L}_\beta, \in) \).
\end{lemma}
\begin{proof}
    Let \( \pi : (M, \in) \to (N, \in) \) be the Mostowski collapse, and set \( \beta = N \cap \mathrm{Ord} \).
    Since \( N \) is transitive, \( \beta \in \mathrm{Ord} \).
    We will prove that \( \beta \leq \delta \) and \( N = \mathrm{L}_\beta \).

    First, suppose \( \delta < \beta \).
    Then \( \delta \in N \), so \( \pi^{-1}(\delta) \in M \).
    Since being an ordinal is absolute between transitive models, \( N \vDash \delta \in \mathrm{Ord} \), so \( M \vDash \pi^{-1}(\delta) \in \mathrm{Ord} \).
    Note that this does not immediately imply that \( \pi^{-1}(\delta) \) is an ordinal in \( \mathrm{V} \) since \( M \) is not necessarily transitive.
    But as \( M \prec \mathrm{L}_\delta \), we obtain \( \mathrm{L}_\delta \vDash \pi^{-1}(\delta) \in \mathrm{Ord} \), and since \( \mathrm{L}_\delta \) is transitive, \( \pi^{-1}(\delta) \) is an ordinal in \( \mathrm{V} \).

    Also, \( M \vDash x \in \pi^{-1}(\delta) \) if and only if \( N \vDash \pi(x) \in \delta \).
    Hence,
    \[ \pi : (\pi^{-1}(\delta) \cap M) \to \delta \]
    is an isomorphism.
    Therefore, the order type of \( \pi^{-1}(\delta) \cap M \) is \( \delta \).
    Let \( f : \delta \to \pi^{-1}(\delta) \cap M \) be a strictly increasing enumeration.
    Then, for any \( \alpha \in \delta \), we must have \( \alpha \leq f(\alpha) < \pi^{-1}(\delta) \).
    Hence \( \delta \leq \pi^{-1}(\delta) \).
    On the other hand, \( \pi^{-1}(\delta) \in M \prec \mathrm{L}_\delta \), so \( \pi^{-1}(\delta) < \delta \).
    This gives a contradiction.

    We now show \( \beta > 0 \).
    Since
    \[ \mathrm{L}_\delta \vDash \exists x.\, \forall y \in x.\, (y \neq y) \]
    the elementary substructure \( M \) must also believe this statement, and so \( N \) does.
    In particular, since \( N \) believes in the existence of an empty set, we must have \( \varnothing \in N \cap \mathrm{Ord} = \beta \) as required.

    We show \( \beta \) is a limit.
    We know that
    \[ \mathrm{L}_\delta \vDash \forall \alpha \in \mathrm{Ord}.\, \exists x.\, x = \alpha + 1 \]
    So \( M \) and hence \( N \) believe this statement.
    Let \( \alpha \in \beta = N \cap \mathrm{Ord} \), then by absoluteness, \( \alpha + 1 \in N \).

    Now we show \( \mathrm{L}_\beta \subseteq N \).
    \[ \mathrm{L}_\delta \vDash \forall \alpha \in \mathrm{Ord}.\, \exists y.\, y = \mathrm{L}_\alpha \]
    So \( N \) satisfies this sentence.
    Since the \( \mathrm{L}_\alpha \) hierarchy is absolute, for all \( \alpha \in N \cap \mathrm{Ord} = \beta \), we have \( \mathrm{L}_\alpha \in N \).

    Finally, we show \( N \subseteq \mathrm{L}_\beta \).
    \[ \mathrm{L}_\delta \vDash \forall x.\, \exists y.\, \exists z.\, y \in \mathrm{Ord} \wedge z = \mathrm{L}_y \wedge x \in z \]
    As \( N \) satisfies this sentence, for a fixed \( a \in N \) there are \( \gamma \in N \) and \( z \in N \) such that
    \[ N \vDash \gamma \in \mathrm{Ord} \wedge z = \mathrm{L}_\gamma \wedge a \in z \]
    By absoluteness, \( a \in \mathrm{L}_\gamma \subseteq \mathrm{L}_\beta \) as required.
\end{proof}
\begin{theorem}
    If \( \mathrm{V} = \mathrm{L} \), then \( 2^{\aleph_\alpha} = \aleph_{\alpha + 1} \) for every ordinal \( \alpha \).
    In particular, \( \mathsf{GCH} \) holds.
\end{theorem}
\begin{proof}
    We will show that \( \mathcal P(\omega_\alpha) \subseteq \mathrm{L}_{\omega_{\alpha + 1}} \).
    Then, as \( \abs{\mathrm{L}_{\omega_{\alpha + 1}}} = \aleph_{\alpha + 1} \), the proof follows.
    To do this, it suffices to show that if \( X \subseteq \omega_\alpha \), then there exists some \( \gamma < \omega_{\alpha + 1} \) such that \( X \in \mathrm{L}_\gamma \).

    Let \( X \subseteq \omega_\alpha \) and let \( \delta > \omega_\alpha \) be a limit ordinal such that \( X \in \mathrm{L}_\delta \).
    Let \( M \) be an elementary submodel of \( \mathrm{L}_\delta \) such that \( \omega_\alpha \subseteq M \), \( X \in M \), and \( \abs{M} = \aleph_\alpha \).
    This exists by the downward L\"owenheim--Skolem theorem.
    By G\"odel's condensation lemma, if \( N \) is the Mostowski collapse of \( M \), then there is a limit ordinal \( \gamma \leq \delta \) such that \( N = \mathrm{L}_\gamma \).
    As \( \abs{N} = \abs{M} = \aleph_\alpha \), we have \( \abs{\mathrm{L}_\gamma} = \aleph_\alpha \), so \( \gamma < \omega_{\alpha + 1} \).
    Finally, as \( \omega_\alpha \subseteq M \), the collapsing map is the identity on \( \omega_\alpha \).
    Thus, the map fixes \( X \), and so \( X \in \mathrm{L}_\gamma \).
\end{proof}
This gives the following theorem.
\begin{theorem}
    \( \Con(\mathsf{ZF}) \) implies \( \Con(\mathsf{ZFC} + \mathrm{V} = \mathrm{L} + \mathsf{GCH}) \).
\end{theorem}
\begin{proof}
    We have shown that there is a definable class \( \mathrm{L} \) such that \( \mathsf{ZF} \) proves
    \[ (\mathsf{ZFC} + \mathrm{V} = \mathrm{L} + \mathsf{GCH})^{\mathrm{L}} \]
    Suppose that \( \mathsf{ZFC} + \mathrm{V} = \mathrm{L} + \mathsf{GCH} \) were inconsistent.
    Then fix \( \varphi \) such that
    \[ \mathsf{ZFC} + \mathrm{V} = \mathrm{L} + \mathsf{GCH} \vdash \varphi \wedge \neg\varphi \]
    Then
    \[ \mathsf{ZF} \vDash (\varphi \wedge \neg\varphi)^L \]
    By relativisation, \( \varphi^L \wedge \neg(\varphi^L) \).
    Hence \( \mathsf{ZF} \) is inconsistent.
\end{proof}
\begin{lemma}[Shepherdson]
    There is no class \( W \) such that
    \[ \mathsf{ZFC} \vdash W \text{ is an inner model} \wedge (\neg\mathsf{CH})^W \]
\end{lemma}
Therefore, the technique of inner models does not let us prove the independence of \( \mathsf{CH} \) from \( \mathsf{ZFC} \).
In order to do this, we will introduce the notion of \emph{forcing}.

\subsection{Combinatorial properties}
\begin{definition}
    Let \( \Omega \) be either a regular cardinal or the class of all ordinals.
    A subclass \( C \subseteq \Omega \) is said to be a \emph{club}, or \emph{closed and unbounded}, if it is
    \begin{enumerate}
        \item \emph{closed}: for all \( \gamma \in \Omega \), we have \( \sup(C \cap \gamma) \in C \);
        \item \emph{unbounded}: for all \( \alpha \in \Omega \) there exists \( \beta \in C \) with \( \beta > \alpha \).
    \end{enumerate}
    A class \( S \subseteq \Omega \) is \emph{stationary} if it intersects every club.
\end{definition}
Note that being a stationary class for \( \mathrm{Ord} \) is not first-order definable.

The property \( \diamondsuit \) states that there is a single sequence of length \( \omega_1 \) which can approximate any subset of \( \omega_1 \) in a suitable sense.
\begin{definition}
    We say that the \emph{diamond principle} \( \diamondsuit \) holds if there is a sequence \( (A_\alpha)_{\alpha < \omega_1} \) such that
    \begin{enumerate}
        \item for each \( \alpha < \omega_1 \), we have \( A_\alpha \subseteq \alpha \); and
        \item for all \( X \subseteq \omega_1 \), the set \( \qty{\alpha \mid X \cap \alpha = A_\alpha} \) is stationary.
    \end{enumerate}
\end{definition}
\begin{lemma}
    \( \mathsf{ZF} \vdash \diamondsuit \to \mathsf{CH} \).
\end{lemma}
\begin{proof}
    If \( (A_\alpha)_{\alpha < \omega_1} \) is a \( \diamondsuit \)-sequence, then for all \( X \subseteq \omega \), there is \( \alpha > \omega \) such that \( X = A_\alpha \).
    Thus \( \qty{A_\alpha \mid \alpha \in \omega_1 \mid A_\alpha \subseteq \omega} = \mathcal P(\omega) \).
\end{proof}
\begin{theorem}
    If \( \mathrm{V} = \mathrm{L} \), then \( \diamondsuit \) holds.
\end{theorem}
\begin{remark}
    \( \diamondsuit \) is used in many inductive constructions in \( \mathrm{L} \) to build combinatorial objects such as Suslin trees.
\end{remark}
\begin{definition}
    Let \( \kappa \) be an uncountable cardinal.
    Then the \emph{square principle} \( \mdwhtsquare_\kappa \) is the assertion that there exists a sequence \( (C_\alpha) \) indexed by the limit ordinals \( \alpha \) in \( \kappa^+ \), such that
    \begin{enumerate}
        \item \( C_\alpha \) is a club subset of \( \alpha \);
        \item if \( \beta \) is a limit ordinal of \( C_\alpha \) then \( C_\beta = C_\alpha \cap \beta \); and
        \item if \( \cf(\alpha) < \kappa \) then \( \abs{C_\alpha} < \kappa \).
    \end{enumerate}
\end{definition}
\begin{theorem}[Jensen]
    If \( \mathrm{V} = \mathrm{L} \), then \( \mdwhtsquare_\kappa \) holds for every uncountable cardinal \( \kappa \).
\end{theorem}
\begin{lemma}
    If \( \mdwhtsquare_{\omega_1} \), then there exists a stationary set \( S \subseteq \qty{\beta \in \omega_2 \mid \cf(\beta) = \omega} \) such that for all \( \alpha \in \omega_2 \) with \( \cf(\alpha) = \omega_1 \), \( S \cap \alpha \) is not stationary in \( \alpha \).
\end{lemma}
\begin{remark}
    If \( \kappa \) is a weakly compact cardinal, then every stationary subset of \( \kappa \) \emph{reflects}: there is \( \alpha \in \kappa \) such that \( S \cap \alpha \) is stationary in \( \alpha \).
    In fact, the claim that every stationary subset of \( \qty{\beta \in \omega_2 \mid \cf(\beta) = \omega} \) reflects at a point of cofinality \( \omega_1 \) is equiconsistent with \( \mathsf{ZFC} \) together with the assertion that there is a Mahlo cardinal.
\end{remark}
